PET

Benchmark
Model:nand v.1 (DTMC)
Parameter(s)N = 60, K = 4
Property:reliable (prob-reach)
Invocation (specific)
./smc.sh nand.prism nand.props -prop reliable -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams S:10000000,Av:10,e:0.001,d:0.05,p:0.05,post:64 -const N=60,K=4
Execution
Walltime:600.1738851070404s
Return code:130
Log
PRISM-games
===========

Version: 2.0.beta3
Date: Thu Mar 19 21:31:33 UTC 2020
Hostname: 68eec9c801d9
Memory limits: cudd=1g, java(heap)=8.9g
Command line: prism nand.prism nand.props -prop reliable -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams 'S:10000000;Av:10;e:0.001;d:0.05;p:0.05;post:64' -const 'N=60,K=4' -javamaxmem 10g

Parsing the model file "nand.prism"...

Parsing properties file "nand.props"...

1 property:
(1) "reliable": P=? [ F s=4&z/N<0.1 ]

Type:        DTMC
Modules:     multiplex 
Variables:   u c s z zx zy x y 

---------------------------------------------------------------------

Model checking: "reliable": P=? [ F s=4&z/N<0.1 ]
Model constants: N=60,K=4
Starting heuristic: RTDP_ADJ
IsMDP false Collapse false break false
ColourParams: S:10000000 Av: 10 eps: 0.001 delta: 0.05 pmin: 0.05
TransDelta: 2.37526000926207E-11
HeuristicSG: Version try0
Grey
======================================